Compiling to Categories

Ok, here's my equation for the solver, written in plain Haskell:

equation :: (Num a, Ord a) => a -> a -> Bool
equation x y =
    x < y &&
    y < 100 &&
    0 <= x - 3 + 7 * y &&
    (x == y || y + 20 == x + 30)

Here's how I run the solver:

    res <- evalZ3With Nothing opts $ do
        x <- mkFreshIntVar "x"
        y <- mkFreshIntVar "y"
        PrimE ast <-
            runKleisli (runZ3Cat (ccc @Z3Cat (uncurry (equation @Int))))
                       (PairE (PrimE x) (PrimE y))
        assertShow ast
        -- check and get solution
        fmap snd $ withModel $ \m ->
            catMaybes <$> mapM (evalInt m) [x, y]
    case res of
        Nothing  -> error "No solution found."
        Just sol -> do
            putStrLn $ "Solution: " ++ show sol

And here's the result, which also show you the equation we submitted to Z3:

(let ((a!1 (ite (<= 0 (+ (- x!0 3) (* 7 y!1)))
                (ite (= x!0 y!1) true (= (+ y!1 20) (+ x!0 30)))
                false)))
  (ite (< x!0 y!1) (ite (< y!1 100) a!1 false) false))

Solution: [-8,2]

Now with one function, I have either a predicate that I can use in Haskell
code, or an input to Z3 for finding possible arguments for which it is true!
</pre>

______________
[1]. https://github.com/conal/concat/issues/4
[2]. http://conal.net/papers/compiling-to-categories/compiling-to-categories.pdf